MIME-Version: 1.0
Server: CERN/3.0
Date: Monday, 06-Jan-97 21:39:36 GMT
Content-Type: text/html
Content-Length: 4568
Last-Modified: Wednesday, 04-Sep-96 03:37:07 GMT


<head><title>ACL2 Version 1.9</title></head>
<!WA0><img src="http://www.cs.utexas.edu/users/sawada/ACL2/logo.gif" align=top ALT="ACL2">

<BR><BR><BR>

<h1>ACL2 Version 1.9</h1>

Copyright (C) 1989-96 
<!WA1><A HREF="http://www.cli.com">Computational Logic, Inc. (CLI)</A>.
All rights reserved.<p>

<h2>ACL2 is a programming language in which you can model computer hardware and
software, as well as a tool to help you prove properties of those models.</h2>

<BR>
The paper <!WA2><A HREF="http://www.cs.utexas.edu/users/reports/bkm96.ps">ACL2 Theorems about Commercial Microprocessors</A>
(with Bishop Brock) briefly discusses the system and two ``industrial
strength'' applications, the Motorola CAP project and the AMD5K86 floating
point division project.  See also <!WA3><A HREF="#Selected References">Selected References</A>.

<BR><BR>
We have two Web browser ``<!WA4><A HREF="http://www.cs.utexas.edu/users/sawada/ACL2/acl2-doc-48.html#The Tours">Tours</A>'' to introduce you to ACL2,
as well as a <!WA5><A HREF="http://www.cs.utexas.edu/users/sawada/ACL2/acl2-doc-1.html#ACL2-TUTORIAL">Tutorial</A>.

<BR><BR>
To obtain ACL2
<ul>
<li>Read the <!WA6><A HREF="http://www.cli.com/ftp/pub/acl2/LICENSE">License Agreement</A> and if you agree to its terms,

<li>download the ACL2 <!WA7><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/acl2.tar.gz">Sources and Documentation</A> and then

<li>follow the <!WA8><A HREF="http://www.cli.com/ftp/pub/acl2/v1-9/README">Installation Instructions</A>.
You may be able to save time by obtaining a
<!WA9><A HREF="#Images">binary image</A> before following the Installation Instructions.

</ul>

<h2>Matt Kaufmann and J Strother Moore</h2>
September 3, 1996<br><br>

<H2><A NAME="Selected References">Selected References</A></H2>

<UL>
<li><!WA10><A HREF="http://www.cs.utexas.edu/users/reports/km94.ps">Design Goals for ACL2</A>
-- an early report identifying aspects of Nqthm of special concern during
the design of ACL2.

<li><!WA11><A HREF="http://www.cs.utexas.edu/users/reports/km96.ps">ACL2:  An Industrial Strength Version of Nqthm</A>
-- how we scaled up the Nqthm (``Boyer-Moore'') logic to Common
Lisp, preserving the use of total functions within the logic but achieving
Common Lisp execution speeds.

<li><!WA12><A HREF="http://devil.ece.utexas.edu:80/~lynch/divide/divide.html">A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating-Point Division Algorithm</A>
(with Tom Lynch) -- the mathematical details of the floating-point
division proof.

<li><!WA13><A HREF="http://www.cs.utexas.edu/users/reports/y96a.ps">Interactive Consistency in ACL2</A>
(by Bill Young) -- an ACL2 translation of Rushby's PVS improvement to
Bevier and Young's Nqthm formalization of the Pease, Shostak and Lamport Oral
Messages (``Byzantine Generals'') problem.

<li><!WA14><A HREF="http://www.cs.utexas.edu/users/reports/y96b.ps">The Specification of a Simple Autopilot in ACL2</A>
(by Bill Young) -- an ACL2 translation of Butler's PVS formalization of a
simple autopilot.

<li><!WA15><A HREF="http://www.cs.utexas.edu/users/reports/bm96.ps">Mechanized Formal Reasoning about Programs and Computing Machines</A>
(by Boyer and Moore) -- explains a formalization style which has
been extremely successful in enabling mechanized reasoning about programs
and machines, illustrated in ACL2.

<li><!WA16><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/acl2-sources/doc/TEX/acl2-book.ps.gz">ACL2 Documentation</A>
-- the complete ACL2 documentation tree in the form of a compressed (gzip'd)
postscript file.  When uncompressed the documentation is approximately 3.5
megabytes of postscript and prints as an 800 page book.  The documentation is
most useful in its HTML or Texinfo forms, where the links in it can be browsed
interactively.  The complete HTML documentation tree is available via the Index
below or organized by
<!WA17><A HREF="http://www.cs.utexas.edu/users/sawada/ACL2/acl2-doc-major-topics.html">Major Topics</A>.
We recommend that you start with the guided <!WA18><A HREF="http://www.cs.utexas.edu/users/sawada/ACL2/acl2-doc-48.html#The Tours">Tours</A>.

</ul>

<!WA19><A HREF="http://www.cs.utexas.edu/users/sawada/ACL2/acl2-doc-index.html"><!WA20><img src=http://www.cs.utexas.edu/users/sawada/ACL2/index.gif></A>

<H2><A NAME="Images">Images</A></H2>

If your machine is listed below, you can avoid rebuilding ACL2 by obtaining a
binary image.  You should nevertheless read the
<!WA21><A HREF="http://www.cli.com/ftp/pub/acl2/LICENSE">License Agreement</A>
and obtain the
<!WA22><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/acl2.tar.gz">Sources and Documentation</A>.
Then download the appropriate image and follow the
QUICK AND EASY INSTALLATION INSTRUCTIONS in
<!WA23><A HREF="http://www.cli.com/ftp/pub/acl2/v1-9/README">Installation Instructions</A>.

<ul>
<li><!WA24><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/images/os-4-sparc-saved_acl2.tar.gz">Sun OS 4.1.3_U1 for Sparc</A>

<li><!WA25><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/images/solaris-2-5-sparc-saved_acl2.tar.gz">Solaris 2.5 for Sparc</A>

<li><!WA26><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/images/solaris-2-5-x86-saved_acl2.tar.gz">Solaris 2.5 for x86</A>

</ul>


